Nuprl Lemma : decidable__assoced
2,24
postcript
pdf
a
,
b
:
. Dec(
a
~
b
)
latex
Definitions
a
~
b
,
Dec(
P
)
,
P
&
Q
,
P
Q
,
b
|
a
,
x
:
A
.
B
(
x
)
,
t
T
Lemmas
divides
wf
,
decidable
divides
,
decidable
and
origin
a, b:
. Dec(a ~ b) a, b:. Dec(a ~ b) 
Qx:A. B(x)
T